MASTERARBEIT
Titel der Masterarbeit
On Hilbert’s Tenth Problem over
Rings of Algebraic Integers
Verfasser
Tim Benedikt Herbstrith
angestrebter akademischer Grad
Master of Science (MSc.)
Wien, im Monat Mai 2018
Studienkennzahl lt. Studienblatt: A 033 821
Studienrichtung lt. Studienblatt: Mathematik
Betreuer: ao. Univ.-Prof. Mag. Dr. Ch. Baxa
https://github.com/tim6her/h10-over-rings-of-integers
Vorwort
Abstract
Contents
1 Prerequisites and central notions 1
2 Hilbert’s tenth problem 55
A Appendix 99
1 Prerequisites and central notions
1.1 Prerequisites from computability theory
{sec:computability theory}
1.1.1 Turing machines, problems, and decidability
01 01
01
2
1 3
≅
3
1
2
↕
𝑥 = 101
≠
𝑦 = 011
↕
{fig:encoding of graphs}
{ex:encoding of graphs}
1
101 011
§
§
0 0 0 1
. . .
overflow
{fig:Turing machine}
_
§_01
start
halt
§ §
§
halt
halt
§
halt
0
0
overow
overow
0
return
1
return
1
overow
0
halt
start
§ _
§__
§001_0_
01
§
_
start
halt
delta
state
state’
delta "state" b = ("state'", b', m)
delta "state" 1 = ("state'", b', m)
delta "state" b = ("state''", b'', m')
state’
state
1
state”
state
1
{lst:add1}
-- start by entering the "overflow" state ...
add1 "start" '§' = ("overflow", '§', 1 )
-- ... and stay in this state, as long as you read only '1'-s
add1 "overflow" '1' = ("overflow", '0', 1 )
-- if you read the first '0' or an empty cell replace it by '1'
-- and enter the "return" state to move the head to the first cell
add1 "overflow" '0' = ("return", '1', -1)
add1 "overflow" '_' = ("return", '1', -1)
-- we finish if we read '§' again or ...
add1 "return" '§' = ("halt", '§', 0 )
-- ... continue to move to the left and don't change the cell
-- content. Here `b` matches '0' or '1'
add1 "return" b = ("return", b , -1)
add1 _state _char = ("error", '_', 0 )
1
{ex:add 1}
add1
start
halt
overow
return
error
add1
error
add1
1101
1 0
01
01
1
https://www.haskell.org/onlinereport/haskell2010
§
1 1 0 1
. . .
start
start
§
overflow
§
§
1 1 0 1
. . .
overflow
overflow
1
overflow
1
§
0 1 0 1
. . .
overflow
overflow
1
overflow
1
§
0 0 0 1
. . .
overflow
overflow
0
return
1
§
0 0 1 1
. . .
return
return
1
return
1
§
0 0 1 1
. . .
return
return
1
return
1
§
0 0 1 1
. . .
return
return
§
halt
§
§
0 0 1 1
. . .
halt
halt
§
halt
§
{fig:complete run}
add1
1101
{ex:finite problems are decidable}
start
halt
accept
reject
start
1
1
1
reject
_
0
0
0
reject
_
_
accept
_
reject
_
_
accept
1
reject
0
accept
reject
{lem:composition of Turing machines}
start
halt
start
§
halt
§
start
halt
start
halt
start
halt
compose
start
compose
halt
halt
start
compose
{ex:tally encoding}
11
-times
1
0
{ex:omega encoding}
01
01
{lst:tally encoding}
-- start by entering the "check" state and ...
tally "start" '§' = ("check", '§', 1 )
-- ... stay in this state while reading only '1'-s
tally "check" '1' = ("check", '1', 1 )
-- on reading '_' accept the input and clear the tape ...
tally "check" '_' = ("accept", '_', -1)
tally "accept" '1' = ("accept", '_', -1)
-- ...except for cell c(1), where you write a '1'
tally "accept" '§' = ("accept", '§', 1 )
tally "accept" '_' = ("halt", '1', -1)
-- however, if you read a '0' first, reject the input
-- by moving to the end of the input string ...
tally "check" '0' = ("rejectMR", '0', 1 )
tally "rejectMR" '_' = ("reject", '_', -1)
tally "rejectMR" b = ("rejectMR", b, 1 ) -- `b` matches '0' or '1'
-- ... and clear the tape except for cell c(1) where you
-- write a '0'
tally "reject" '§' = ("reject", '§', 1 )
tally "reject" '_' = ("halt", '0', -1)
tally "reject" b = ("reject", '_', -1) -- `b` matches '0' or '1'
tally _state _char = ("error", '_', 0 )
01
1
tally
start
halt
check
accept
reject
rejectMR
error
1
0
{ex:tally pairing}
11
-times
0 11
-times
0 1
0
1
{ex:total pairing}
01
01
§
§
b
1
b
2
. . .
b
n−2
b
n−1
b
n
. . .
find non-empty
The machine finds the first non-empty cell.
{fig:total pairing non empty}{sub@fig:total pairing non empty}
§
b
1
b
2
. . .
b
n−2
b
n−1
b
n
. . .
shift left b
n
The machine shifts the content of each cell one cell to the left …
{fig:total pairing shift left 1}{sub@fig:total pairing shift left 1}
§
b
1
b
2
b
3
. . .
b
n−1
b
n
. . .
shift left b
1
… until it reaches the end of tape symbol §.
{fig:total pairing shift left 2}{sub@fig:total pairing shift left 2}
§
b
1
b
2
b
3
. . .
b
n−1
b
n
. . .
find __
The machine finds two consecutive blank cells and starts over.
{fig:total pairing double blank}{sub@fig:total pairing double blank}{fig:pairing function}
0
{lem:minimization}
§
__
__
§
_
_
_
{pro:characterizations of ce sets}
1 1
1 1
§
_
§
_
{lst:check one}
1
-- start by entering the "check" state
check1 "start" '§' = ("check", '§', 1 )
-- if you read a 1, check that the next cell is blank, and accept
check1 "check" '1' = ("check_blank", '1', 1 )
check1 "check_blank" '_' = ("accept", '_', -1)
-- if either of these conditions is not the case, reject
check1 "check" b = ("reject", b, 1 )
check1 "check_blank" b = ("reject", b, 1 )
-- accepting and rejecting actions
check1 "accept" 1 = ("halt", 1, -1)
check1 "reject" b = ("error", b, 1)
check1 _state _char = ("error", '_', 0 )
1 1
{pro:Posts theorem}
10 01
1
1
10100
0
0
0
0
0
1 0
1
0
1
1
1 0
halt
1.1.2 Church-Turing thesis and the halting problem
2
2
{fig:Pinocchio}
1
0
0
{{eq:m reducibility}}{{eq:m reducibility}}
{pro:m reducibility and decidability}
1.2 Prerequisites from model theory
{sec:model theory}
1.2.1 Formulae and models
1
e
1
e
01
01
1
e
1
e
1
e
0 0
0
1
0
1
x
i
x
1
x
1
x
2
x
2
1
x
2
1
x
2
2
1
x
2
i
x
i
x
i
x
1
x
n
x
1
x
n
x
1
x
n
x
1
x
n
x
1
x
n
x
i
x
1
x
n
x
1
x
n
x
1
x
n
x
1
x
n
x
1
x
n
x
1
x
n
{lem:terms of rings are polynomials}
0 1
x
i
1 1 1
-times
0 1 1 1
-times
a x
i
1
x
i
d
a
m
1
m
k
m
i
3
4
x
1
x
2
x
3
x
2
x
1
x
2
1
{ex:formula distributivity}
x
1
x
2
x
3
x
1
x
2
x
3
x
1
x
3
x
2
x
3
3
4
x
1
x
1
x
1
x
1
x
2
x
3
x
1
x
2
x
1
x
2
x
3
x
i
x
i
x
i
x
i
x
i
x
i
x
1
x
2
x
3
x
2
x
1
x
1
x
n
x
1
x
n
x
1
x
n
x
1
x
n
x
1
x
n
x
2
x
2
x
1
x
2
x
2
x
2
x
3
x
1
x
2
x
1
x
2
x
2
x
4
x
3
x
1
1.2.2 Morphisms, theories, and decidability
{sec:theories}
x
1
x
1
e x
1
x
1
e x
1
x
1
x
1
x
2
x
3
x
1
x
2
x
3
x
1
x
2
x
3
x
1
x
1
x
1
1
e
x
1
x
1
1
x
1
e
{thm:elementary equivalence}
Th
H10
x
i
1
x
i
k
x
i
1
x
i
k
Th
x
i
1
x
i
k
x
i
1
x
i
k
is atomic, and
x
1
x
1
0x
2
x
1
x
2
1
Th
Th
x
1
x
2
1
1 0
Th
Th
1
2
4
3
x
1
x
2
x
3
Ex
1
x
2
Ex
2
x
3
Ex
3
x
1
x
1
x
2
x
3
Th
c
c
H10
x
i
1
x
i
k
x
i
1
x
i
k
x
i
1
x
i
k
x
i
1
x
i
k
is atomic, and
there exists an atomic formula with
, or and
{thm:Diophantine theory}
P
P
P
H10
c
x
i
1
x
i
d
P P
x
i
1
x
i
k
x
i
1
x
i
k
x
i
1
x
i
k
x
i
1
x
i
k
0
x
i
1
x
i
k
H10
x
i
1
x
i
k
x
i
1
x
i
k
x
i
1
x
i
k
x
x
j
x
-times
s
x
x
1
x
1
0
x
0 1
s
H10
∗
(𝔄)
Th
∃+
(𝔄)
Th(𝔄)
𝐷(𝔄)
H10(𝔄)
𝐷
∃+
(𝔄)
𝐷
𝑐
(𝔄)
Th
H10
H10
H10
∗
(𝔄)
Th
∃+
(𝔄)
Th(𝔄)
𝐷(𝔄)
H10(𝔄)
𝐷
∃+
(𝔄)
𝐷
𝑐
(𝔄)
𝒦
1.2.3 Computable structures and decidable models
{sec:computable structures}
ar
{lem:properties of Goedelization}
x
i
x
i
x
i
FC R
F
R
C
1
1
11011
0 1 1
{ex:polynomials are computable}
{ex:Z is computable}
{thm:computable categoricity}
{ex:N is computably categorical}
0
0
c
n1
c
n
1
c
n
{lem:H10 is semi decidable}
H10
x
1
x
n
x
1
x
n
H10
1.3 Prerequisites from number theory
{sec:number theory}
1.3.1 Number fields and rings of algebraic integers
{thm:integral closure}
{pro:characterization of integral elements}
{pro:being integral is transitive}
{thm:K is the quotient field of O K}
{thm:primitive element}
{thm:norm and trace}
{cor:O K is computable}
1.3.2 Ideals of
5
5
{thm:algebraic integers are Dedekind domain}
prime ideal
6
prime ideal
prime ideal
prime ideal
{thm:Chinese remainder}
6
prime ideal
1.3.3 Geometry of numbers
𝐷
𝑒
1
𝑒
2
{fig:lattice}
7
{thm:Minkowski}
7
{pro:Lagranges four square theorem}
{thm:Dirichlet}
8
{thm:Dirichlet approximation}
8
ႼႵᆡ
ႼႴᆡ ႼႳᆡ
ႼႲᆡ Ⴒᆡ
Ⴓᆡ Ⴔᆡ
Ⴕᆡ
ႼႴᆡ
ႼႳᆡ
ႼႲᆡ
Ⴒᆡ
Ⴓᆡ
Ⴔᆡ
Ⴑ
ᆂ
{fig:dirichlet}
0
1
;
0 + ℤ = 1 + ℤ
{fig:unitcircle}
{{eq:Kronecker 1}}{{eq:Kronecker 1}}
{thm:Kronecker}
{{eq:Kronecker 3}}{{eq:Kronecker 3}}
{{eq:Kronecker 2}}{{eq:Kronecker 2}}
{{eq:Kronecker 4}}{{eq:Kronecker 4}}
1.3.4 Absolute values and local fields
{thm:Hasse Minkowski}
{lem:quadratic form}
{thm:strong approximation}
2 Hilbert’s tenth problem
2.1 Different perspectives on an old problem
2.1.1 Diophantine equations and sets
1
2
3
1
0
1 0
1 0
1
2
3
α α
{ex:Diophantine sets}
{ex:being non zero is Diophantine}
{ex:U K is Diophantine}
{ex:N is Diophantine over Z}
x
1
x
n
y
1
y
m
y
1
y
m
y
1
y
m
H10
H10
{lem:intersections and unions}
H10
2.1.2 Purely Diophantine sets
x
1
x
n
y
1
y
m
y
1
y
m
y
1
y
m
{pro:Diophantine singletons}
{thm:purely Diophantine sets}
H10
H10
∗
(𝔒
𝐾
)
Th
∃+
(𝔒
𝐾
)
Th(𝔒
𝐾
)
𝐷(𝔒
𝐾
)
H10(𝔒
𝐾
)
𝐷
∃+
(𝔒
𝐾
)
𝐷
𝑐
(𝔒
𝐾
)
𝒦
2.1.3 Related problems
Th
4
Th
{thmt@@DPRM@data}
{thmt@@DPRM}{thm:DPRM}
{cor:H10 over Z}
H10
4
y
1
y
m
y
1
y
m
{{eq:representing halting set}}{{eq:representing halting set}}
H10
H10
H10
2.2 Some structural results
{lem:moving up}
{cor:Diophantine theory is undecidable}
H10
{{eq:halting set is Diophantine}}{{eq:halting set is Diophantine}}
H10
H10
H10
{thm:CE sets are Diophantine}
101
-times
-times
{thm:strong vertical method}
{{eq:sigma x and norm of y}}{{eq:sigma x and norm of y}}
{{eq:sigma alpha and norm of y}}{{eq:sigma alpha and norm of y}}
{{eq:x mod alpha}}{{eq:x mod alpha}}
{lem:8}
{lem:approximations of embeddings are Diophantine}
2.3 Hilbert’s tenth problem over totally real number fields and
number fields with one pair of non-real embeddings
2.3.1 Finitely many easy lemmas
{{eq:Pell}}{{eq:Pell}}
{{eq:def of x and y}}{{eq:def of x and y}}
5
5
even
odd
even
odd
{lem:epsilon is unit}
{lem:x and y solve Pells equation}
{lem:real part of epsilon}
{lem:addition formulas}
{lem:y m divides y mk}
{lem:x m and y m are relative prime}
odd
{lem:recursion for x_m and y_m}
{lem:m congruent y m}
{lem:a congruent b mod c}
{lem:congruence x_2m+k}
{lem:forcing divisibility}
{lem:subgroup of ker N L/K}
{lem:rank of N_L/K U_L}
-times
{{eq:rank of G}}{{eq:rank of G}}
2.3.2 Diophantine definition of over
{lem:L over K is quadratic}
{{eq:approximations of a}}{{eq:approximations of a}}
{{eq:def of sigma ij}}{{eq:def of sigma ij}}
{lem:r and s for tr and opnr}
{lem:properties of sigma epsilon}
{lem:modulus of sigma epsilon}
{lem:approx for delta i 1}
{lem:approx for delta i 2}
{lem:modulus of elements in the kernel}
{lem:approximation of epsilon with a}
{lem:epsilon is not a root of unity}
by (iv)
{{eq:approximation of epsilon 0}}{{eq:approximation of epsilon 0}}
{pro:epsilon essentially generaltes G}
{cor:forcing sequences}
{{eq:forcing solutions to be sequences}}{{eq:forcing solutions to be sequences}}
even
odd
{lem:m smaller x m}
{lem:approximations of sigma x and sigma y}
{{eq:approximation of sigma x and sigma y}}{{eq:approximation of sigma x and sigma y}}
{lem:defining e}
{{eq:def of e}}{{eq:def of e}}
{{eq:norm of x eh and x er}}{{eq:norm of x eh and x er}}
Lem. 2.3.3.(ii)
even
odd
{lem:congruences for x m}
{{eq:approx of x r1 x r2 and x m}}{{eq:approx of x r1 x r2 and x m}}
{{eq:norm of p x}}{{eq:norm of p x}}
{{eq:norm of x r1 plus x r2}}{{eq:norm of x r1 plus x r2}}
{{eq:norm of x m and x r1 plus x r2 1}}{{eq:norm of x m and x r1 plus x r2 1}}
{{eq:norm of x m and x r1 plus x r2 2}}{{eq:norm of x m and x r1 plus x r2 2}}
{lem:def of b}
{{eq:sequences}}{{eq:sequences}}
{{eq:force sequences}}{{eq:force sequences}}
{{eq:force sequences for w and z}}{{eq:force sequences for w and z}}
{{eq:approx of embeddings 1}}{{eq:approx of embeddings 1}}
{{eq:approx of embeddings 2}}{{eq:approx of embeddings 2}}
{{eq:v is non zero}}{{eq:v is non zero}}
{{eq:z 2 divides v}}{{eq:z 2 divides v}}
{{eq:cong 1}}{{eq:cong 1}}
{{eq:cong 2}}{{eq:cong 2}}
{{eq:cong 3}}{{eq:cong 3}}
{{eq:divisibilty of z}}{{eq:divisibilty of z}}
{{eq:approx of embeddings 2 v2}}{{eq:approx of embeddings 2 v2}}
{{eq:v is non zero v2}}{{eq:v is non zero v2}}
{{eq:z 2 divides v v2}}{{eq:z 2 divides v v2}}
{{eq:cong 1 v2}}
{{eq:cong 1 v2}}
{{eq:cong 2 v2}}{{eq:cong 2 v2}}
{{eq:cong 3 v2}}{{eq:cong 3 v2}}
{{eq:j congruent xsi mod y eh}}{{eq:j congruent xsi mod y eh}}
{{eq:k congruent j mod m}}{{eq:k congruent j mod m}}
{cor:ZZ is Diophantine over O K}
H10
H10
A Appendix
{sec:Appendix}
A.1 Collected Haskell implementations
A.1.1 Simulating Turing machines
{app:turing}
https://github.com/
tim6her/h10-turing-machines
git clone https://github.com/tim6her/h10-turing-machines.git
cd h10-turing-machines
cabal setup && cabal build && cabal install
ghci
>>> import Automaton.TuringMachine
>>> :l tally
>>> let d = toTransition tally "error" -- mark the errornous state
>>> let turing = TuringMachine "start" '_' "halt" d
>>> "§1111" >>> turing -- Tally encoding of 4
Just "§1"
>>> "§1011" >>> turing -- Not tally encoded
Just "§0"
A.1.2 Polynomials
{app:polynomials}
{lst:monomials}
{-# LANGUAGE RebindableSyntax #-}
module Monomial
( Monomial
, (<*>)
, idt
, mfromList
, clean
) where
import NumericPrelude
import Data.Map (Map, delete, empty, foldrWithKey, fromList, member, insert,
insertWith, (!))
import Algebra.Monoid as Monoid
import Test.Tasty
import Test.Tasty.HUnit
import Test.Tasty.QuickCheck as QC
-- | Monomials are mappings from ZZ to NN with finite support
newtype Monomial = Monomial (Map Integer Integer) deriving (Eq, Ord)
instance Monoid.C Monomial where
idt = Monomial empty
(<*>) = mmul
instance Show Monomial where
show (Monomial m)
| m == empty = "1"
| otherwise = foldrWithKey
(\x e sh -> "X" ++ show x ++ "^" ++ show e ++ " " ++ sh)
"" m
-- | Creates monomials from list of tuples
--
-- Left entry is index of indeterminate, right index is power of the
-- indeterminate
--
-- === Example
-- >>> mfromList [(1, 2), (0, 3), (4, 7)]
-- X0^3 X1^2 X4^7
mfromList :: [(Integer, Integer)] -> Monomial
mfromList l = clean $ Monomial $ fromList l
-- | Multiplies two monomials
--
-- === Example
-- >>> mmul (mfromList [(1, 2), (2, 4)]) (mfromList [(2, 1), (3, 2)])
-- X1^2 X2^5 X3^2
mmul :: Monomial -> Monomial -> Monomial
mmul xx@(Monomial m1) yy@(Monomial m2)
| m1 == empty = yy
| m2 == empty = xx
| otherwise = clean $ Monomial $ foldrWithKey
(\x e m -> if x `member` m
then insertWith (+) x e m
else insert x e m)
m2 m1
clean :: Monomial -> Monomial
clean (Monomial m)
| m == empty = (Monomial m)
| otherwise = Monomial $ foldrWithKey
(\x e m -> if e <= 0
then delete x m
else m)
m m
-- * Testing
main :: IO ()
main = defaultMain tests
tests :: TestTree
tests = testGroup "Tests" [properties, unitTests]
properties :: TestTree
properties = testGroup "Properties" [qcProps]
qcProps = testGroup "Axioms of monoids"
[ QC.testProperty "left multiplication by identity" $
\x -> (let m = mfromList (x :: [(Integer, Integer)])
in idt <*> m == m)
, QC.testProperty "right multiplication by identity" $
\x -> (let m = mfromList (x :: [(Integer, Integer)])
in m <*> idt == m)
, QC.testProperty "associativity" $
\x y z -> (let m1 = mfromList (x :: [(Integer, Integer)])
m2 = mfromList (y :: [(Integer, Integer)])
m3 = mfromList (z :: [(Integer, Integer)])
in (m1 <*> m2) <*> m3 == m1 <*> (m2 <*> m3))
, QC.testProperty "commutativity" $
\x y -> (let m1 = mfromList (x :: [(Integer, Integer)])
m2 = mfromList (y :: [(Integer, Integer)])
in m1 <*> m2 == m2 <*> m1)
]
unitTests = testGroup "Unit tests"
[ testCase "show X0^3 X1^2 X4^7" $
show (mfromList [(1, 2), (0, 3), (4, 7)]) @?= "X0^3 X1^2 X4^7 "
, testCase "sample multiplication" $
show (mmul (mfromList [(1, 2), (2, 4)]) (mfromList [(2, 1), (3, 2)])) @?=
"X1^2 X2^5 X3^2 "
, testCase "test clean" $
mfromList [(1, 0), (2, 0), (3, 1)] @?= mfromList [(3, 1)]
]
{lst:polynomials}
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
import NumericPrelude
import qualified Monomial
import qualified Data.Map as Map
import Algebra.Monoid as Monoid
import Algebra.Ring as Ring
import Algebra.Module as Module
import Algebra.Additive as Additive
import Test.Tasty
import Test.Tasty.HUnit
import Test.Tasty.QuickCheck as QC
-- | Polynomials over a ring R are finitely supported functions
-- from the set of monomials to R
newtype Polynomial a = Polynomial (Map.Map Monomial.Monomial a)
-- | Polynomials form an additive (abelian) group
instance (Ring.C a, Eq a) => Additive.C (Polynomial a) where
zero = Polynomial Map.empty
(+) = padd
negate (Polynomial m) = Polynomial $ Map.map negate m
-- | Polynomials from an R-module
instance (Ring.C a, Eq a) => Module.C a (Polynomial a) where
(*>) 0 _ = zero
(*>) a (Polynomial m) = Polynomial $ Map.map (a*) m
-- | Polynomials form a ring with unit
instance (Ring.C a, Eq a) => Ring.C (Polynomial a) where
one = pfromList [(1, [])]
(*) p@(Polynomial m1) q
| p == zero = zero
| q == zero = zero
| p == one = q
| q == one = p
| otherwise = Map.foldrWithKey
(\mono coeff poly -> (coeff *> mono `mmul` q) + poly)
0 m1
-- | Two polynomials are equal if their difference is zero
instance (Ring.C a, Eq a) => Eq (Polynomial a) where
(==) p q = let (Polynomial m) = p - q in m == Map.empty
instance (Show a, Eq a) => Show (Polynomial a) where
show (Polynomial p)
| p == Map.empty = "0"
| otherwise = Map.foldrWithKey
(\m a sh -> show a ++ " " ++ show m ++ "+ " ++ sh)
"" p
-- | Adds two polynomials over the same ring
--
-- If a coefficient of a monoid equals 0 the monoid is dropped out of the map
padd :: (Ring.C a, Eq a) => Polynomial a -> Polynomial a -> Polynomial a
padd p@(Polynomial m1) q@(Polynomial m2)
| m1 == Map.empty = q
| m2 == Map.empty = p
| otherwise = clean $ Polynomial $ Map.foldrWithKey
(\mono coeff poly -> if mono `Map.member` poly
then Map.insertWith (+) mono coeff poly
else Map.insert mono coeff poly)
m2 m1
mmul :: (Ring.C a, Eq a) => Monomial.Monomial -> Polynomial a -> Polynomial a
mmul mono poly@(Polynomial mp)
| mono == Monomial.idt = Polynomial mp
| poly == zero = zero
| otherwise = Polynomial $ Map.mapKeys (mono Monomial.<*>) mp
-- | Generate polynomials from lists
pfromList :: (Ring.C a, Eq a) => [(a, [(Integer, Integer)])] -> Polynomial a
pfromList [] = zero
pfromList ((a, m):l) = deepClean . clean $ (Polynomial $ Map.singleton
(Monomial.mfromList m) a) + pfromList l
-- | Comfort function for creating polynomials
--
-- === Example
-- >>> 2 *> ((x 1 + x 2) * (x 1 - x 2)) == 2 *> x 1 ^ 2 - 2 *> x 2 ^ 2
-- True
x :: (Ring.C a, Eq a) => Integer -> Polynomial a
x i = pfromList [(1, [(i, 1)])]
-- | Remove monoids with coefficient zero from support
clean :: (Ring.C a, Eq a) => Polynomial a -> Polynomial a
clean (Polynomial m) = Polynomial $ Map.foldrWithKey
(\mono coeff poly -> if coeff == 0
then Map.delete mono poly
else poly)
m m
-- | Remove variables with power zero from monomials
--
-- This function runs in O(n log(n)) so use it sparsely
deepClean :: (Ring.C a, Eq a) => Polynomial a -> Polynomial a
deepClean (Polynomial m) = Polynomial $ Map.mapKeys Monomial.clean m
-- * Testing
main :: IO ()
main = defaultMain tests
tests :: TestTree
tests = testGroup "Tests" [properties, unitTests]
properties :: TestTree
properties = testGroup "Properties" [qcAddProps, qcModProps,
localOption (QuickCheckTests 5) qcRingProps,
qcAlgebraProps]
qcAddProps = testGroup "Group axioms for addition"
[ QC.testProperty "addition is commutative" $
\x y -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
q = pfromList (y :: [(Int, [(Integer, Integer)])])
in p + q == q + p)
, QC.testProperty "addition is associative" $
\x y z -> (let p1 = pfromList (x :: [(Int, [(Integer, Integer)])])
p2 = pfromList (y :: [(Int, [(Integer, Integer)])])
p3 = pfromList (z :: [(Int, [(Integer, Integer)])])
in (p1 + p2) + p3 == p1 + (p2 + p3))
, QC.testProperty "addition by zero" $
\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in p + zero == p)
, QC.testProperty "addition with inverse" $
\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in p - p == zero)
]
qcModProps = testGroup "Module axioms"
[ QC.testProperty "first distributive law" $
\a x y -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
q = pfromList (y :: [(Int, [(Integer, Integer)])])
in (a :: Int) *> (p + q) == a *> q + a *> p)
, QC.testProperty "second distributive law" $
\a b x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in (a + b :: Int) *> p == a *> p + b *> p)
, QC.testProperty "multiplications commute" $
\a b x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in (a * b :: Int) *> p == a *> (b *> p))
, QC.testProperty "multiplication by one" $
\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in (one :: Int) *> p == p)
]
qcRingProps = testGroup "Ring axioms"
[ QC.testProperty "multiplication is associative" $
\x y z -> (let p1 = pfromList (x :: [(Int, [(Integer, Integer)])])
p2 = pfromList (y :: [(Int, [(Integer, Integer)])])
p3 = pfromList (z :: [(Int, [(Integer, Integer)])])
in (p1 * p2) * p3 == p1 * (p2 * p3))
, QC.testProperty "left multiplication by one" $
\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in one * p == p)
, QC.testProperty "right multiplication by one" $
\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in p * one == p)
, QC.testProperty "distributive law" $
\x y z -> (let p1 = pfromList (x :: [(Int, [(Integer, Integer)])])
p2 = pfromList (y :: [(Int, [(Integer, Integer)])])
p3 = pfromList (z :: [(Int, [(Integer, Integer)])])
in p1 * (p2 + p3) == p1 * p2 + p1 * p3)
]
qcAlgebraProps = testGroup "Algebra axioms"
[ QC.testProperty "multiplications commute" $
\x y a -> (let p1 = pfromList (x :: [(Int, [(Integer, Integer)])])
p2 = pfromList (y :: [(Int, [(Integer, Integer)])])
in (a :: Int) *> (p1 * p2) == (a *> p1) * p2)
]
unitTests = testGroup "Unit tests"
[ testCase "sample polynomial" $
show (pfromList [(1, [(1, 2), (3, 4)]), (-4, [(1, 4), (2, 3)])]
:: Polynomial Int) @?= "1 X1^2 X3^4 + -4 X1^4 X2^3 + "
, testCase "test equality" $
pfromList [(0, [(1, 1)])] @?= (zero :: Polynomial Int)
]
Bibliography
http://www.jstor.org/stable/2269326
10.2307/2371045
10 . 2307 / 2318447
http://www.jstor.org/stable/2318447
10. 1016/ j .amc .2005. 09.066
https://doi.org/10.1016/j.amc.2005.09.066
10.2307/1998133
10.2307/2040720
10.1112/jlms/s2-18.3.
385
10.1515/crll.1988.388.189
https://doi.org/10.1515/crll.1988.388.189
10.1112/jlms/s1-8.1.18
10.1007/BF01700692 https://doi.org/10.1007/BF01700692
10.1090/S0273-0979-00-00881-8
10.1007/978- 3- 642-
75306-0
10.1215/S0012-7094-36-00227-2 https://doi.org/10.
1215/S0012-7094-36-00227-2
10.1007/978-3-642-54936-6_5
10.1007/978-1-4613-0041-0
https://doi.org/10.1007/978-1-4613-0041-0
https://
www.ebook.de/de/product/3665990/david_marker_model_theory_an_introduction.
html
www.jmilne.org/
math/
http://www.logic.univie.ac.at/~muellem3/TCS.pdf
http : / / ubdata .
univie.ac.at/AC05622932
10.4310/MRL.2013.v20.
n5.a12
10.2307/2047021
https://doi.org/10.2307/2047021
http://www.ams.org/
notices/200803/tx080300344p.pdf
10.1007/3- 540-
45455-1_4
10.1090/S0002-
9904-1944-08111-1 https://doi.org/10.1090/S0002-9904-1944-08111-1
10.2307/2266510
10.2307/2033628 https://doi.
org/10.2307/2033628
10.2307/2266685
10.2307/2269028
10.1515/crll.1986.368.127
https://doi.org/10.1515/crll.1986.368.127
10.1002/cpa.3160420805 https://doi.org/10.1002/cpa.3160420805
10 .
1002/cpa.3160420703
https://doi.org/
10.1090/conm/270/04370
http : / / www . ebook . de / de / product / 6433593 /
alexandra_shlapentokh _ hilbert_s_tenth_problem_diophantine_classes_and_
extensions_to_global_fields.html
http://math.
cornell.edu/~shore/papers/pdf/proc4t.pdf
10.1016/S0049-237X(99)
80028-7 http://www.sciencedirect.com/science/article/pii/S0049237X99800287
http://eudml.org/doc/212515
10.1112/plms/s2-42.1.230 https://doi.org/10.1112/plms/s2-42.1.230
Todo list
